MENTAL vs. CÁLCULO LAMBDA DE CHURCH

Un modelo teórico para las expresiones funcionales
“La mayoría de los lenguajes de programación tienen sus raíces en el cálculo lambda” (Peter Landin)

---

El Cálculo Lambda, de Church
Conceptos fundamentales

El cálculo lambda o cálculo-λ (lambda calculus o λ-calculus), creado por el matemático, lógico y filósofo Alonzo Church en los años 1930s, es un modelo teórico formal para las expresiones funcionales, es decir, funciones definidas a partir de otras funciones.

Las funciones del cálculo lambda son objetos matemáticos con las siguientes características:

• Las funciones no tienen nombre (son anónimas).
  
  
• Las funciones pueden ser argumentos de otras funciones.
  
  
• El resultado de una función es otra función.
  
  
• Hay transparencia referencial: el significado de una expresión funcional depende únicamente del significado de las subexpresiones funcionales.
  
  
• Se diferencia claramente entre la definición de una función y su aplicación (o evaluación):
  
  
  • La definición de una función consta de dos partes. En la primera se especifican los nombres de los parámetros. En la segunda se especifica el cuerpo de la función.
    
    
  • En la aplicación de una función se sustituyen los parámetros de la función por los valores de los argumentos.

Esta distinción se hace necesaria, pues por ejemplo la expresión matemática x+5 no indica si se trata de una función de la variable x o un cálculo con el valor de x. Este problema se resuelve mediante la llamada “notación lambda”. En el caso de una función de una variable, la notación es λx.f(x), en donde:

• El símbolo λ indica que se trata de la definición de una función.
  
  
• La variable x que aparece tras λ es la variable (o parámetro) formal.
  
  
• f(x) es una expresión en la que aparece x (el cuerpo de la función).

Su aplicación se realiza mediante (λx.f(x))a = f(a) siendo a el argumento. Por ejemplo: (λx.axb)3 = a3b

Para dos variables, la notación es:

• Definición de función: λxy.f(x, y)
  
  
• Aplicación: (λxy.f(x, y))(a, b) = f(a, b)
  Ejemplo: (λxy.xyx)(3, 4) = 343

En general, para n variables, la notación es:

• Definición de función: λx₁ ... x_n.f(x₁, ... , x_n)
  
  
• Aplicación: (λx₁ ... x_n.f(x₁, ... , x_n))(a₁, ... ,a_n) = f(a1, ... , a_n)

La definición de una función recuerda a una expresión cuantificada universalmente, en el que λ desempeña un papel similar a ∀ (para todo).

Los nombres de las variables de las expresiones funcionales es irrelevante. Es por ello que se dice que las variables de la función son ficticias o falsas. Por ejemplo, λxy.x+y y λuv.u+v son equivalentes.


Variables ligadas y libres

En una expresión lambda, una variable x es ligada o libre, según aparezca como parámetro o no, respectivamente, en la definición de la función. Ejemplos:

1. En la expresión funcional (λx.xy), x es una variable ligada e y es libre.
   
   
2. En la expresión funcional (λxy.xyx), x e y son variables ligadas.

Variables como funciones

Las variables x, y, z,… también se consideran funciones o autofunciones, es decir, que se aplican a sí mismas y se devuelven a sí mismas. En este sentido, la expresión f(x) se suele escribir fx para abreviar, pues se considera que es la aplicación de la función f a la función x. Análogamente,

fxy = (fx)y
fxyz = ((fx)y)z (supone asociatividad a la izquierda) ...

Por ello, una expresión funcional de n variables se suele escribir λx₁ ... x_n.fx₁...x_n.


Evaluación parcial

Para toda función lambda de n variables, es posible definir una versión “curry” −nombre que viene del lógico Haskell B. Curry− equivalente, en la que se van aplicando los argumentos en serie, uno tras otro. Por ejemplo, la versión curry de λxyz.xyz es λx.λy.λz.xyz. Este proceso se denomina “currificación”. En ambos casos, los argumentos hay que especificarlos en el mismo orden y el resultado es el mismo, pero la sintaxis es distinta:

• Versión normal, con aplicación simultánea o concurrente de los argumentos:
  
  (λxyz.xyz)abc = abc
  
  
• Versión curry:
  
  (λx.λy.λz.xyz)abc
  
  Esta expresión se interpreta siempre con asociatividad a la izquierda y en donde van desapareciendo progresivamente las variables instanciadas:
  
  (((λx.λy.λz.xyz)a)b)c = (((λy.λz.ayz)b)c = (λz.abz)c = abc

Por lo tanto, en el cálculo lambda, todas las funciones de n parámetros se pueden considerar como una expresión de funciones de un solo parámetro.


Sustitución de variables por argumentos

En la aplicación de una función a unos argumentos, se realiza una sustitución de cada parámetro por su correspondiente argumento. Para indicar esto, el cálculo lambda utiliza la notación [N/x]M, que indica que en la expresión M queremos sustituir la variable x por la expresión N. Ejemplos:

[u/x]x = u
[u/x](x y) = (u y)
[(λx.x)/x]x = (λx.x)

Si en M no aparece la variable x, entonces M queda invariable: [N/x]M = M. Por ejemplo, [u/x]y = y.

Evidentemente, por la propia definición de aplicación de función, se tiene que

(λx.M)N = [N/x]M

Es la llamada “reducción β”, “conversión β” o “axioma β” del cálculo lambda.

Si la expresión N aparece en M como variable falsa, se le puede asignar un nuevo nombre antes de realizar la sustitución. Por ejemplo:

[u/x](λu.x) = [u/x](λz.x) = λz.u

Es la llamada “conversión α” o “axioma α” y se realiza mediante

λx.M = λz.[z/x]M (supone z ligada en M)

La “conversión η” expresa la idea de que dos funciones f y g son iguales si y solo si dan el mismo resultado para todos los posibles argumentos. Es decir, fa = ga para todo argumento a. Si x no aparece en el cuerpo de f ni el de g, entonces fx = gx.


Cálculos como reducciones

Los cálculos en el cálculo lambda son reducciones sucesivas, aplicando en cada paso la conversión β, hasta que se llega a la forma más simple posible. Una expresión que puede reducirse se denomina “redex” (reduction expresion). Una redex puede contener otras redex. Una expresión que no puede reducirse (que no contiene ningún redex) se dice que se encuentra en “forma normal”.

El teorema de Church-Rosser del cálculo lambda establece que el resultado de un cálculo no depende del orden en el que se aplican las reducciones (sustituciones β), es decir, todas las posibles secuencias de reducciones avanzan hacia el mismo resultado final, que es el mismo que se obtiene cuando se aplican las reducciones de forma concurrente.


Ejemplos de funciones simples

• Identidad (I): I := λx.x
  Ejemplo: (λx.x)a = a
  
  
• Primero (Prim): Prim := λxy.x
  Ejemplo: (λxy.x)ab = a
  
  
• Segundo (Seg): Seg := λxy.y Ejemplo: (λxy.y)ab = b
  
  
• Constante (K): K := λx.k Ejemplo: (λx.k)a = k
  
  
• Duplicación (Dup): Dup := λx.xx Ejemplo: (λx.xx)a = aa

Funciones de orden superior

Si tenemos la expresión de n variables λx₁ ... x_n.fx₁ ... x_n

• fx₁ ... x_n puede ser, a su vez, una expresión lambda.
• Las variables x₁ ... x_n pueden ser también expresiones lambda.
• Los argumentos pueden ser expresiones lambda.

Entonces aparecen entonces las funciones de orden superior.

Un ejemplo simple es la composición de dos funciones es λgfx.g(fx). Que es equivalente a g○f en notación matemática tradicional (primero se aplica f y luego se aplica g). Por ejemplo:

f := λx.xax   g := λx.bxb
(fg) = λx.xax(λx.bxb) = λx.bxbaλx.bxb
(fg)c = (λx.bxbaλx.bxb)c = bcbabcb
(gf) = λx.bxb(λx.xax) = bλx.xaxb
(gf)c = (bλx.xaxb)c = bcacb

Algunas leyes de composición de funciones son:

• Autoaplicación de la función “identidad” (I):
  (I I) = (λx.x)(λx.x) = λx.x = I
  
  
• Autoaplicación de la función “duplicación” (Dup):
  (Dup Dup) = (λx.xx)(λx.xx) = (λx.xx)(λx.xx) = (Dup Dup)
  (se produce un bucle infinito con el mismo resultado)
  
  
• Autoaplicación de la función “segundo” (Seg):
  (Seg Seg) = (λxy.y)(λxy.y) = (λy.y) = I

Aritmética

Sustituyendo en λx.fx, x por fx, tenemos: λfx.f(fx)

Esta es la definición de una función que, actuando sobre cualquier función fx, produce la misma función iterada dos veces, es decir, f(fx). Esta es la función identificada con el símbolo 2 (en negrita, para diferenciarlo del número 2).

2 = λfx.f(fx)

Análogamente,

3 = λfx.f(f(fx))
4 = λfx.f(f(f(fx)))
...

Junto con:

0 = λfx.x (función que devuelve siempre la variable x)

1 = λfx.fx (función identidad: devuelve la misma función)

En general, un número n en el cálculo lambda es una función que tiene como argumento otra función f y que produce como resultado la n-aria composición de f. Estos números se llaman “numerales de Church”. Ejemplos:

(0)(xa) = x
(1)(xa) = xa
(2)(xa) = xaa
(3)(xa) = xaaa
...

Un aspecto sorprendende de los numerales de Church es la posibilidad de definir las operaciones aritméticas de suma, multiplicación y potencia en términos de funciones aplicadas a numerales. La suma se basa en la operación Sucesor (Suc), definida así: (Suc n) := λnfx.f(nfx)

• Suma.
  (Suma n₁ n₂) = λn₁n₂.n₁(Suc n₂)
  n₁+n₂ es el resultado de aplicar la función sucesor n₁ veces a n₂.
  Ejemplo: (Suma 2 3) = 2+3 = 5
  
  
• Producto.
  (Prod n₁ n₂) = λn₁n₂.n₁(Suma n₂ 0)
  n₁*n₂ es el resultado de sumar n₂ y 0, n₁ veces.
  Ejemplo: (Prod 2 3) = 2*3 = 6
  
  
• Potencia.
  (Pot n₁ n₂) = λn₁n₂.n₁(Prod n₂ 1)
  n₁^n₂ es el resultado de multiplicar n₂ y 1, n₁ veces.
  Ejemplo: (Pot 2 3) = 2^3 = 9

Así como la expresión de sucesor de un numeral (Suc n) es relativamente simple, el Predecesor Pn, es decir n−1, es mucho más compleja:

Pn = λnfx.n(λgh.h(gf)( λu.x)( λu.u)

Funciones lógicas

Las funciones lógicas se pueden también definir mediante expresiones lambda. Una función lógica es una función que tiene como parámetros los valores lógicos V (verdadero) o F (falso) y que produce un valor lógico como resultado.

Los valores V y F se definen así:

V := λxy.x (devuelve el primer argumento)
F := λxy.y (devuelve el segundo argumento)

Y las operaciones lógicas se definen de la siguiente manera:

And: ∧ := λxy.xyF
Or: ∨ := λxy.xVy
Not ¬ := λx.xFV

Ejemplos:

∧VF = (λxy.xyF)VF = VFF = (λxy.x)FF = F

∨VF = (λxy.xVy)VF = VVF = (λxy.x)VF = V

¬V = (λx.xFV)V = VFV = (λxy.x)FV = F

Gracias a las definiciones anteriores de V y F como funciones se puede especificar la condición lógica If-Then-Else, mediante una expresión lambda con 3 variables: b (valor de verdad), t (rama Then) y e (rama Else):

IfThenElse := λb.λt.λe.bte

(IfThenElse V p q) = p (devuelve rama Then)

(IfThenElseF p q) = qV (devuelve rama Else)

Predicados

Un predicado se define como una función que devuelve un valor de verdad. Un ejemplo de predicado es la función Z, que tiene como parámetro un numeral y que devuelve V si el argumento es el numeral 0, y F si es cualquier otro numeral:

Z := λn.nF¬F
Z0 = (λn.nF¬F)0 = 0F¬F = ¬F = V
Zn = (λn.nF¬F)n = nF¬F = IF = F

En donde hay que tener en cuenta:

0 = λfx.x
0fa = (λfx.x)fa = a. Por lo tanto, 0F¬ = ¬
Fa = (λfxy.y)a = λy.y = I. Por lo tanto, F¬ = I
nF es la función F aplicada n veces. Pero según lo anterior, nF = I.

Funciones recursivas

Queremos calcular, por ejemplo, la factorial de un número:

f(n) = (if n=1 then 1 else n*f(n−1))

El problema es que en el cálculo lambda no se permiten funciones recursivas porque las funciones son anónimas y, por lo tanto, no pueden llamarse a sí mismas. Sin embargo, es posible definirlas mediante el combinador Y (también llamado “combinador de punto fijo” o “combinador paradójico”), descubierto por Haskell B. Curry, que se define de la manera siguiente:

Y = λy.(λx.y(x x))(λx.y(x x))

Aplicando Y a una función R se tiene:

YR = λx.R(x x)(λx.R(x x)) = R(λx.R(x x))(λx.R(x x)) = R(YR)

Es, decir, YR es igual a la función R aplicada a YR. Aquí aparece la recursividad, pues

YR = R(YR) = R(R(R(YR)))...

Mediante Y se pueden codificar funciones recursivas. Por ejemplo, para resolver el problema del factorial, definimos una función g (de manera informal):

g = λf. λn.if n=1 then 1 else n*f(n−1)

g(n) devuelve 1 si n=1 y n*f(n−1) si n≠1.

La función recursiva es g(Yg)n. Por ejemplo, para n=4:

g(Yg)4 = (λn.if n=1 then 1 else n*((Yg)(n−1)))4 =
if n=4 then 1 else 4*((Yg)(4−1))) = 4*((Yg) 3) =
4*(g(Yg) 3) = 4*(λn.if n=1 then 1 else n*((Yg)(n−1)))3 =
4*(if n=3 then 1 else 3*((Yg)(3−1))) = 4*(3*(Yg) 2)) =
4*(3*(g(Yg) 2) =
4*(3*(λn.if n=1 then 1 else n*((Yg)(n−1)))2 =
4*(3*(if n=1 then 1 else 2*((Yg)(2−1))) = 4*(3*(2*(Yg) 1)) = 4*(3*(2*(λn.if n=1 then 1 else 1*((Yg)(1−1)))1 =
4*(3*(2*(1*))) = 4*3*2*1

La solución formal en cálculo lambda consiste en sustituir las expresiones condicionales y las aritméticas por las correspondientes expresiones lambda basadas en numerales:

n−1 → Pn (predecesor de n)
n*(n−1) → (Prod n Pn)
if n=1 then 1 else n*f(n−1) → ((Z Suc(n)) 1 (Prod n Pn))

Por lo tanto, la expresión recursiva es g(Yg)n, con

g = λf.((Z Suc(n)) 1 (Prod n Pn))

MENTAL vs. Cálculo Lambda
Paradigmas

Cálculo lambda.

Es un modelo teórico monoparadigma. Todo es una función: los números, la aritmética, la lógica, etc. Por lo tanto, toda estructura de información hay que crearla cada vez que se necesita. La única estructura de información que contempla es la secuencia dentro de una expresión funcional, estructura que no es explícita, sino implícita.

Church tenía al principio un objetivo mucho mas ambicioso: construir un sistema formal completo y un lenguaje universal para modelizar toda la matemática. Pero cuando vio que la paradoja de Russell le afectaba, rebajó su objetivo inicial para centrarse exclusivamente en modelar la computabilidad mediante expresiones funcionales.

MENTAL.

Es un modelo teórico de paradigma universal que contempla todo tipo de paradigmas y todo tipo de expresiones, y que incluye un espacio abstracto donde se almacenan las expresiones y que permanecen.

Con MENTAL se logra el objetivo inicial de Church de crear un lenguaje universal para modelizar toda la matemática.

Primitivas

Cálculo lambda.

El cálculo lambda se considera un formalismo de máxima economía conceptual matemática, y el lenguaje teórico de programación más simple que existe, porque solo utiliza dos primitivas: 1) la definición de funciones; 2) la aplicación de funciones mediante la sustitución de las variables por los argumentos. Con estas dos primitivas, el cálculo lambda permite expresar de manera precisa cualquier función computable.

MENTAL.

Hay 12 primitivas semánticas universales, con sus correspondientes contrarias o duales. No existe ninguna primitiva “función”. Las funciones son expresiones derivadas de las primitivas.

Nivel de abstracción

Cálculo lambda.

El hecho de usar solo dos primitivas implica un bajo nivel de abstracción. Todo requiere mucho detalle.

MENTAL.

El nivel de abstracción conceptual es supremo. Todo es más sencillo, más expresivo, más compacto y directo, pues se trabaja directamente con arquetipos primarios.

Expresiones

Cálculo lambda.

Solo contempla expresiones funcionales. Los parámetros de las funciones deben declararse explícitamente delante del cuerpo de la función. No pueden asignarse nombres a las funciones, lo que conduce a graves dificultades expresivas. Tampoco admite funciones simples como λx.x+1, pues las operaciones aritméticas no son primitivas.

MENTAL.

Contempla todo tipo de expresiones. Las expresiones funcionales equivalentes a las del cálculo lambda son expresiones genéricas parametrizadas. Los parámetros se declaran en negrita y dentro del propio cuerpo de la expresión. Esto tiene la ventaja de que se pueden manipular como cualquier variable. Por ejemplo, un parámetro se puede convertir en una variable normal, una variable en parámetro, etc. Por ejemplo:

z = ⟨( f(x y) = x+y+2 )⟩
z/(x=a y=b) // ev. ⟨( f(a b) = a+b+2 )⟩

z = ⟨( f(a b) = a+b+2 )⟩
z/(a=x b=y) // ev. ⟨( f(x y) = x+y+2 )⟩

Cualquier expresión puede actuar como una función mediante el mecanismo de particularización. Por ejemplo,

(z = x+y+2)
z/(x=3 y=4) // ev. 9
z/(x=3) // ev. y+5

Se pueden especificar funciones con nombre y anónimas. Por ejemplo:


1. ⟨( f(n) = (2*n + 1) )⟩ // definición función parametrizada con nombre
f(3) // ev. 7 (aplicación)
   
   
2. f=(2*n + 1) // definición de función no parametrizada con nombre
f/(n=3) // ev. 7 (aplicación)
   
   
3. (2*n + 1)/(n=3) // ev. 7 (definición y aplicación de función sin nombre)

Las expresiones genéricas de MENTAL van más allá de lo funcional, pues permiten definir reglas lógicas, procedimientos, expresiones modales, imaginarias, etc. Representan un nivel “meta” sobre las expresiones “base”. Los sucesivos niveles “meta” corresponden a las expresiones genéricas de orden superior.

Variables ligadas y libres

Cálculo lambda.

Las variables ligadas se especifican delante del cuerpo de la expresión, de la misma forma que con el cuantificador universal de la lógica de predicados. Por ejemplo, en λxy.xaxby, las variables x e y son ligadas, y a y b son libres.

MENTAL.

Une los conceptos de cuantificación universal y parametrización. El cuantificador universal, que antes estaba asociado a la lógica, pasa a ser algo universal aplicable a todo tipo de expresiones, incluidas las funciones. Los parámetros aparecen dentro de la expresión genérica. Esto implica que la expresión es autosuficiente, al no depender de algo externo, y la notación es más simple e intuitiva. Por ejemplo, en la expresión ⟨x+y+z+1⟩, x e y son parámetros y z es una variable no parametrizada.

En las expresiones no genéricas, no se especifica ninguna variable como parámetro. Esto supone mayor flexibilidad, pues unas veces las variables actuarán como parámetros y otras veces no.

Aritmética

Cálculo lambda.

Las operaciones aritméticas y los numerales de Church son funciones.

MENTAL.

La operación primitiva es la “Suma” (junto con su contraria “Resta”), que es de tipo general, es decir, puede sumar todo tipo de expresiones y no solo números. El resto de las operaciones aritméticas son derivadas.

Los numerales de Church es un buen ejercicio teórico, pero es un grave error considerar los números como funciones.

Sustitución β

Cálculo lambda.

Sustituye los parámetros por los argumentos en el cuerpo de la función. Establece la forma de sustituir en el cuerpo de la función cada parámetro por su opuesto. La regla es:

λx.M N = [N/x]M

MENTAL.

Los parámetros pueden ser sustituidos por otras expresiones cualesquiera, sin restricción alguna. La aplicación de una función a unos argumentos se puede realizar de varias formas.


1. f(5)/⟨(f(n) = 2*n + 1)⟩ // ev. 11
2. (2*n + 1)/(n=5) // ev. 11
3. z=(2*n + 1)
4. z/(n=5) // ev. 11

En general, la expresión del cálculo lambda [N/x]M equivale en MENTAL a M/(x=N). En el cálculo lambda, si x no existe en M, el resultado es M. En MENTAL la expresión se autoevalúa. Por ejemplo,

(M = axb)
M/(y=c) // se autoevalúa
M // ev. axb

La “curryficación” se puede especificar así:

(x+y+1)/(x=a)/(y=b) // ev. (a+y+1)/(y=b) ev. a+b+1

La asociatividad por defecto es a la izquierda.

El equivalente a una redex es una expresión que no se autoevalúa. El equivalente a una forma normal es una expresión que se autoevalúa.

Conversión α

Cálculo lambda.

El axioma es: λx.M = λz.[z/x]M (supone z ligado en M)
(sustituir, en M, z por x)

MENTAL.

En una expresión genérica parametrizada, los nombres de los parámetros pueden ser cualesquiera. Además, no se confunden con las variables normales. Por ejemplo, en la expresión ⟨x+x+1⟩, x es un parámetro y x es una variable. Por lo tanto, la conversión α no es necesaria.

Conversión η

La conversión η no es necesaria, ni se necesita ningún formalismo especial, porque a nivel conceptual se ve que las expresiones siguientes (por ejemplo) son iguales, y no solo funciones, sino expresiones en general:

⟨( f(x y) = (x+y x*y) )⟩
f(2 3) // ev. (5 6)
(x+y x*y)/(x=3 y=3) // ev. (5 6)

Evaluación parcial

Cálculo lambda.

Está limitada a funciones y a variables ligadas.

MENTAL.

Se puede realizar en todo tipo de expresiones, con variables ligadas o no. Ejemplos:


1. (x+y+2)/(x=3) // ev. 5+y
   
   
2. ⟨( f(x y) = x+y x*y) )⟩
⟨( g(y) = f(5 y) )⟩ // ev. ⟨( g(y) = 5+y 5*y )⟩
   
   
3. ⟨( f = x+y+2 )⟩
⟨( g(y) = f/(x=5) )⟩ // ev. ⟨( g(y) = 7+y )⟩

Recursión

Cálculo lambda.

Una función no puede ser recursiva, es decir, no puede llamarse a sí misma porque las funciones son anónimas. Para solucionar este problema se acude a algo complejo y artificial como es el combinador de punto fijo Y.

MENTAL.

Permite asignar nombres (incluso parametrizados) a expresiones, simplificando así las expresiones y permitiendo la recursión de forma natural, directa e intuitiva. Por ejemplo:

⟨( fac(n) = 1 ← n=1 →' n*fac(n−1) )⟩ // factorial de n

Computación paralela

Cálculo lambda.

No contempla computación paralela.

MENTAL.

Permite computación paralela de una manera muy simple mediante la mera conjunción de procesos.

Implementación

Cálculo lambda.

El cálculo lambda implica tratar a las funciones como objetos de primera clase, lo que hace que compleja la implementación.

MENTAL.

La implementación es simple porque se basa en conceptos muy simples.

Tipos

Cálculo lambda.

Kleene y Rosser (1936) demostraron que el cálculo lambda era inconsistente. Entonces, Church desarrolló (1940) una teoría funcional simple de tipos, una teoría más simple que la que la que apareció en Principia Mathematica. El cálculo lambda original de Church no tenía tipos, por lo que las funciones podían aplicarse sin restricciones. La teoría de tipos simples es computacionalmente menos potente pero más consistente a nivel lógico.

En la teoría de tipos de Church, las expresiones funcionales se clasifican en tipos, y los tipos restringen las posibles formas combinatorias de dichas expresiones. Los tipos son categorías de funciones y juegan un papel análogo al de los tipos de conjuntos en teoría de conjuntos.

MENTAL.

Los tipos no son necesarios en ningún tipo de expresiones (funciones, conjuntos, predicados, etc.) porque cuando hay autorreferencias, el resultado es una expresión fractal, es decir, una expresión descriptiva de tipo recursivo. La teoría de tipos de Church como la teoría de tipos de Russell es innecesaria porque no se pueden producir paradojas.

Fundamentación

Cálculo lambda.

Se utiliza como modelo teórico de los lenguajes de programación funcionales.

MENTAL.

Es un modelo teórico universal, un lenguaje universal, un paradigma universal y una fundamentación universal, capaz de expresar todo tipo de paradigmas.

Modelo computacional

Cálculo lambda.

Aportó un modelo computacional. Una función F: n → n entre números naturales es computable si y solo si existe una función lambda f tal que si F(n₁) = n₂, entonces fn₁ = n₂.

MENTAL.

Es un modelo teórico universal.

Conclusiones
Church, con el cálculo lambda, realizó numerosas aportaciones al campo de la computación, entre ellas:

• La definición formal de computabilidad de una manera abstracta, independientemente de ninguna implementación concreta. El modelo computacional se basa en: 1) dos primitivas funcionales (definición y aplicación de funciones) que permiten definir todo tipo de funciones: 2) la semántica de función como proceso de transformación de argumentos en un resultado.
  
  
• Las funciones sin nombre (funciones lambda). Y la posibilidad de que una función se invoque a sí misma, pese a no tener nombre (la recursividad).
  
  
• Los números como funciones (los numerales de Church) y las operaciones aritméticas como funciones.
  
  
• Las operaciones lógicas como funciones.
  
  
• Los valores lógicos (V y F) como funciones, que permiten implementar la condición lógica (If-Then-Else).
  
  
• Los predicados como funciones que devuelven un valor de verdad.

Sin embargo, el cálculo lambda −como la máquina de Turing y la teoría de categorías− es un ejemplo de incumplimiento del principio de la navaja de Einstein: “Hay que hacer todo lo más simple posible, pero no más simple”. Utiliza como único concepto el de expresión funcional, con dos aspectos: definición de una función y aplicación de una función. Esto conduce a graves dificultades expresivas. Todo es una función, lo que produce que los conceptos derivados (números, predicados, valores de verdad, operaciones aritméticas, operaciones lógicas, condiciones, etc.) se expresen de manera compleja y antinatural.

---

Adenda
Church y sus contribuciones a la ciencia

El cálculo lambda fue desarrollado en los años 1930s por Alonzo Church [1941] para formalizar las funciones computables, es decir, para definirlas de forma precisa: toda función numérica computable es computable mediante el cálculo lambda, utilizando los correspondientes numerales de Church en lugar de los números. El cálculo lambda es un modelo teórico de computación, que tiene una potencia computacional equivalente al de una máquina de Turing.

Cuando se inventó el cálculo lambda, los ordenadores todavía no existían. Sin embargo, se puede considerar el primer lenguaje de programación funcional de la historia. Ha sido el fundamento de muchos lenguajes funcionales, habiendo tenido gran influencia en el diseño de los lenguajes de programación en general.

Lisp fue el primer lenguaje en aplicar el cálculo lambda [McCarthy, 1960], por lo que es el lenguaje funcional más antiguo y popular. Está orientado al cálculo simbólico y se aplica principalmente a temas de inteligencia artificial.

Al Lisp le siguieron, entre otros, Scheme, ML, Miranda y Haskell. De todas formas, lenguajes funcionales “puros” son solo Haskell y Miranda. Y lenguajes híbridos (funcionales con otras características, normalmente imperativas) son Lisp, Scheme y ML.

Las contribuciones principales de Church han sido dos:

1. La tesis de Church.
   Afirma que toda función numérica efectivamente computable es recursiva y computable por el cálculo lambda. Sustituye de esta forma a la noción informal de “computación”.
   
   A finales de 1936, Turing, que había estado también trabajando sobre el tema de la computabilidad, publicó su famoso artículo “On computable numbers ...” en el que expone la tesis de que toda función computable es computable por un dispositivo teórico que hoy se conoce como “máquina de Turing”. El propio Turing demostró que ambos modelos computacionales eran equivalentes. La tesis se denomina de Church-Turing, una tesis que conecta los aspectos operacionales, epistémicos y extrínsecos de la aritmética con los aspectos ontológicos, intrínsecos y abstractos. Esta tesis establece también los límites de la computabilidad, pues toda computación está limitada por las primitivas utilizadas (por Church o por Turing).
   
   
2. El teorema de Church.
   Church, estudiando “el problema de decisión de Hilbert” (Entscheidungsproblem) le condujo a lo que se conoce como “teorema de Church”. Este teorema afirma que no existe ningún algoritmo o procedimiento mecánico capaz de decidir si las proposiciones de la aritmética son verdaderas o falsas. Por lo tanto, que no existe una solución general al problema de decisión. Esto equivale a que la lógica de predicados de primer orden es indecidible.
   
   Church también usó el cálculo lambda para resolver por primera vez el problema de saber si dos expresiones funcionales cualesquiera del cálculo lambda son o no equivalentes. Este problema también es indecidible: no puede ser resuelto por una expresión funcional general del propio cálculo lambda. Esta cuestión fue planteada antes incluso del problema de la parada de una máquina de Turing. Church y Turing estuvieron muy influenciados por el teorema de incompletud de Gödel.

En el año 1990 se celebró un simposio en honor de Church en la State University of New York at Bufalo, por sus contribuciones seminales a los fundamentos de la teoría de la computación.


Los combinadores de punto fijo

Un punto fijo de una función f(x) es un valor v de x tal que f(v) = v. Por ejemplo, 0 y 1 son puntos fijos de f(x) = x², porque 0² = 0 y 1² = 1. Un punto fijo de una función de orden superior f(g) es otra función h tal que f(h) = h. Como YR = R(YR), entonces YR es un punto fijo de cualquier función R.

El combinador de punto fijo Y de Curry no es el único que existe en el cálculo lambda. De hecho, el cálculo lambda sin tipos posee infinitos combinadores de punto fijo. En 2005, Mayer Goldberg [2005] demostró que el conjunto de combinadores de punto fijo del cálculo lambda es recursivamente numerable. En el cálculo lambda con tipos −más restrictivo a nivel combinatorio− no existe ningún combinador de punto fijo.

El uso de combinadores de punto fijo para la recursión se denomina “recursión anónima”.


Bibliografía

• Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam, 1984. [Tratado exahustivo, texto estándar].
  
  
• Church, Alonzo. The Calculi of Lambda Conversion. Annals of Mathematicals Studies, No. 6. Princeton University Press, Princeton, New Jersey, 1941.
  
  
• Goldberg, Mayer. On the Recursive Enumerability of Fixed-Point Combinators. BRICS Report RS-05-1, University of Aarhus, 2005.
  
  
• Hindley, J. Roger; Seldin, Jonathan P. Lambda-Calculus and Combinators. An Introduction. Cambridge University Press, 2008.
  
  
• Landin Peter. A Correspondence Between ALGOL 60 and Church's Lambda-Notation. Communications of the ACM, 8 (2): 89-101, 1965.
  
  
• McCarthy, John. Recursive Functions of Symbolic Expressions and their Computation by machine, Part I. Coms. of the ACM, vol. 3, no. 4, pp. 184-195, April 1960.
  
  
• Michaelson, Greg. An Introduction to Functional Programming Through Lambda Calculus. Dover, 2011. Cambridge University Press, 2009.
  
  
• Revesz, G.E. Lambda-calculus, Combinators and Functional Programming. Cambridge University Press, 2009.
  
  
• Rosser, J.B. Highlights of the history of the lambda calculus. Annals of the History of Computing, 6:4, 337-349, 1984.
  
  
• Stoy, Joseph E. Denotational Semantics. The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, Massachusetts, 1981.